es:ES, e:E, l:IdLnk. loc-ordered(es;es-receives(es;e;l)) 

latex

Definitions

x:AB(x), P & Q, (e <loc e'), x f y, x:A. B(x), x:AB(x), P  Q, P  Q, IdLnkDeq, es-eq(es), rcv-from-on(dE;dL;info;e;l;r), x.A(x), eventlist(pred?;e), receives(dE;dL;pred?;info;p;e;l), es-receives(es;e;l), EOrderAxioms(E; pred?; info), Prop, IdLnk, e < e', left+right, x:A. B(x), P  Q, sender(e), rcv?(e), Type, a<b, , {x:A| B(x) }, f(a), x before y  l, l-ordered(T;x,y.R(x;y);L), loc-ordered(es;L), ES, es-pred?(es), es_info(es), Id, E, es-oaxioms(es), 1of(t), sends-bound(p;e;l), t  T, pred(e), s = t, first(e), b, A, A & B, SWellFounded(R(x;y)), pred!(e;e'), (e < e'), Void, R1 => R2, False

Lemmas

rel plus monotone, pred! wf, es-loc-pred-plus, IdLnk wf, event system wf, l before wf, es-receives wf, es-pred!-wellfounded, nat wf, not wf, first wf, pred wf, assert wf, rcv? wf, sender wf, sends-bound wf, es-oaxioms wf, EOrderAxioms wf, l before filter, eventlist wf, rcv-from-on wf, Id wf, es-eq wf, idlnk-deq wf, es info wf, l before eventlist iff, es-E wf, es-pred? wf